home *** CD-ROM | disk | FTP | other *** search
/ Sprite 1984 - 1993 / Sprite 1984 - 1993.iso / lib / tex / inputs / vdm.sty (.txt) < prev    next >
LaTeX Document  |  1991-05-20  |  38KB  |  937 lines
  1. %    VDM documentstyle option for LaTeX
  2. %    M. Wolczko 
  3. %    Created from the ashes of VDM.tex and CBJ's vdm86.tex
  4. %    Uses the AMS msym fonts if available: if you don't have them,
  5. %    follow the instructions near the string FONT-CUSTOMIZING.
  6. %    $Log:    vdm.doc,v $
  7. %    Revision 2.5  88/03/25  18:52:29  mario
  8. %    Improved use of AMS fonts.
  9. %    Improved efficiency by eliminating unnecessary macros.
  10. %    Enable line breaks after underscores in math mode.
  11. %    Fixed used of penalties....were in wrong placeto have any effect.
  12. %    Added \uniqueval, \cons, formbox environment, \R
  13. %    Fixed composite environments so that they can be used in horizontal
  14. %    mode.
  15. %    Fixed a bug in the proof environment.
  16. %    Revision 2.4  87/11/12  12:31:07  mario
  17. %    Shortened lines for network mailers,
  18. %    Changed mathcodes of digits,
  19. %    Added \Rat, changed \DEF, added betweenFunctionAndPre hook,skip,
  20. %    and penalty, added \Conc
  21. %    Revision 2.3  87/02/26  11:36:07  miw
  22. %    Absence of a blank line after \end{vdm} now forces \noindent.
  23. %    Can now have pre- and post-conditions in function defns.
  24. %    Added \mapinto macro.
  25. %    Revision 2.2  86/12/18  12:00:17  miw
  26. %    Added \@changeMathmodeCatcodes to \begin{vdm} to avoid as many
  27. %    catcode problems with @ and _ as possible.
  28. %    Fixed a bug in \If (was adding extra blank lines).
  29. %    Added the \nexists macro.
  30. %    Added the *-form of fn (which had been inadvertently omitted).
  31. %    Fixed a bug in the proof environment (had a name clash with latex).
  32. %    Revision 2.1  86/11/24  13:08:34  miw
  33. %    **** MAJOR REWRITE/EXTENSION ****
  34. %    Entry to the vdm env now is a no-op!
  35. %    No mathcode changes to get the right letters in math mode.
  36. %    Double quotes now delimit text in math mode.
  37. %    \baselineskip within vdm mode is now \VDMbaselineskip.
  38. %    Added the \amssy font.
  39. %    Vertical VDM things (ops, fns, etc) shouldn't need blank lines
  40. %    around them. 
  41. %    Let the user choose whether some things are left- or right-aligned.
  42. %    Added *-forms of quantifiers.
  43. %    Added composite env and \scompose.
  44. %    Added proof env.
  45. %    Revision 1.8  86/10/08  14:11:36  miw
  46. %    Changed \or, \rd, \wr to \Or, \Rd, \Wr.
  47. %    Changed keyword font to sans-serif.
  48. %    Changed \makeNewKeyword to use \newcommand.
  49. %    Added \where keyword.
  50. %    Changed \Nat, \Int, \Bool, \Real to use `blackboard' font.
  51. %    Added `Strachey brackets' using \term.
  52. %    Added function composition, \compf.
  53. %    Added a *-form to the fn environment to omit parens on args.
  54. %    Added a *-form to \LambdaFn to place body on a new line.
  55. %    Added \min and \max monadic operators.
  56. %    Changed \serd and \busd to \rres and \rsub.
  57. %    Added \const for constants.
  58. %    Revision 1.7  86/08/14  17:52:32  miw
  59. %    Fixed bugs in vdmfn and vdmop.
  60. %    Moved the pre..Hooks in operations and functions to occur earlier
  61. %    (allows one to change baselineskip).
  62. %    Revision 1.6  86/06/03  12:23:05  miw
  63. %    Added the formula env, and fixed a bug in \type.
  64. %    Revision 1.5  86/05/07  17:51:48  miw
  65. %    Parameterised more vertical skips.  Changed many dimensions from pts
  66. %    to exs.  Fixed a bug in \type.  Altered externals so that field names
  67. %    are flush right.
  68. %    Revision 1.4  86/04/17  11:09:04  miw
  69. %    Tweaked some more.
  70. %    Revision 1.3 86/03/14 20:44:22 miw
  71. %    Added left margin control with \VDMindent.
  72. %    Tweaked some penalties (esp. \hyphenpenalty)---first use of a
  73. %    \discretionary in quantified expresssion.
  74. %    Fixed a bug in IndentedPara (using box0 instead of copy0)
  75. %    Revision 1.2  86/03/12  16:26:23  miw
  76. %    Changed the fn env. and \Cases.  Added \@raggedRight.
  77. %    Fixed lots of other minor things.
  78. %    Revision 1.1  86/03/03  18:42:40  miw
  79. %    Initial revision
  80. %    $Header: vdm.doc,v 2.5 88/03/25 18:52:29 mario Locked $
  81. %----------------------------------------------------------------
  82. %    Installation-dependent features
  83. % FONT-CUSTOMIZING
  84. \newif\ifams@
  85. \ams@true  % change to \ams@false if you don't have the AMS fonts
  86. %\ams@false  % change to \ams@true if you have the AMS fonts
  87. \newif\ifps@ \ps@false % PostScript-based
  88. \def\@fmtname{lplain}
  89. \def\@psfmtname{pslplain}
  90. \def\@testcmsy{\if@usecmsy \else 
  91.   \@latexerr{Can't use vdm with this PSLaTeX}%
  92.     {This PSLaTeX does not have the CMSY symbols
  93.     available, and cannot be used with VDM style.  Get
  94.     a guru to rebuild PSLaTeX with the CMSY and CMMI
  95.     fonts included.}\fi}
  96. \def\@testcmmi{\if@usecmmi \else
  97.   \@latexerr{Can't use vdm with this PSLaTeX}%
  98.     {This PSLaTeX does not have the CMMI symbols
  99.     available, and cannot be used with VDM style.  Get
  100.     a guru to rebuild PSLaTeX with the CMSY and CMMI
  101.     fonts included.}\fi}
  102. \ifx\fmtname\@fmtname % standard LaTeX is OK
  103. \else \ifx\fmtname\@psfmtname \global\ps@true \@testcmsy \@testcmmi
  104.       \else \ams@false \fi\fi % don't use AMS for SliTeX
  105. \newfam\msxfam
  106. \newfam\msyfam
  107. \ifams@
  108.     % this is lifted from amssymbols.sty
  109.     \ifcase\@ptsize
  110.      \font\tenmsx=msxm10
  111.      \font\sevenmsx=msxm7
  112.      \font\fivemsx=msxm5
  113.      \font\tenmsy=msym10
  114.      \font\sevenmsy=msym7
  115.      \font\fivemsy=msym5
  116.      \font\tenmsx=msxm10 scaled \magstephalf
  117.      \font\sevenmsx=msxm8
  118.      \font\fivemsx=msxm6
  119.      \font\tenmsy=msym10 scaled \magstephalf
  120.      \font\sevenmsy=msym8
  121.      \font\fivemsy=msym6
  122.      \font\tenmsx=msxm10 scaled \magstep1
  123.      \font\sevenmsx=msxm8
  124.      \font\fivemsx=msxm6
  125.      \font\tenmsy=msym10 scaled \magstep1
  126.      \font\sevenmsy=msym8
  127.      \font\fivemsy=msym6
  128.     \textfont\msxfam=\tenmsx  \scriptfont\msxfam=\sevenmsx
  129.       \scriptscriptfont\msxfam=\fivemsx
  130.     \textfont\msyfam=\tenmsy  \scriptfont\msyfam=\sevenmsy
  131.       \scriptscriptfont\msyfam=\fivemsy
  132.     \def\hexnumber@#1{\ifnum#1<10 \number#1\else
  133.      \ifnum#1=10 A\else\ifnum#1=11 B\else\ifnum#1=12 C\else
  134.      \ifnum#1=13 D\else\ifnum#1=14 E\else
  135.      \ifnum#1=15 F\fi\fi\fi\fi\fi\fi\fi}
  136.     \def\msx@{\hexnumber@\msxfam}
  137.     \def\msy@{\hexnumber@\msyfam}
  138. %----------------------------------------------------------------
  139. %    The vdm environment
  140. \def\vdm{\@changeMathmodeCatcodes\@postUnderPenalty10000 }
  141. % after an \end{vdm} the next paragraph is not indented unless a \par
  142. % comes first
  143. \def\endvdm{\global\let\par=\@undonoindent
  144.   \global\everypar={{\setbox0=\lastbox}\global\everypar={}%
  145.             \global\let\par=\@@par}}
  146. \def\@undonoindent{\global\everypar={}\global\let\par=\@@par\@@par}
  147. %-----------------------------------------------------------------
  148. %     Controlling line and page breaks
  149. % Text within the vdm environment is essentially mathematical in
  150. % nature, so requires special care.  Whenever outer vertical mode is
  151. % entered, the \@beginVerticalVDM command should be used.  This sets
  152. % up \leftskip, \rightskip, \baselineskip, \lineskip and
  153. % \lineskiplimit to conform with the overall style.
  154. % When entering unrestricted horizontal mode, the \@beginHorizontalVDM
  155. % command should be used.  This sets up:
  156. %    \leftskip and \rightskip to 0,
  157. %    \\ to do line breaking
  158. %    ragged right line breaking, with special penalties, and
  159. %    enters math mode.
  160. % \@endHorizontalVDM should be called when leaving unrestricted
  161. % horizontal mode.
  162. \def\@beginVerticalVDM{\@changeMargins\@changeBaselineskip}
  163. \def\@beginHorizontalVDM{\@restoreLineSeparator
  164.   \@restoreMargins\@raggedRight\noindent$\strut\relax}
  165. \def\@endHorizontalVDM{\relax\strut$}
  166. % \VDMindent is used for \leftskip within VDM, \VDMrindent for
  167. % \rightskip, \VDMbaselineskip for \baselineskip
  168. \newdimen\VDMindent \VDMindent=\parindent
  169. \newdimen\VDMrindent \VDMrindent=\parindent
  170. \def\VDMbaselineskip{\baselineskip}
  171. \def\@changeMargins{\leftskip=\VDMindent \rightskip=\VDMrindent}
  172. \def\@restoreMargins{\advance\hsize by-\leftskip
  173.   \advance\hsize by-\rightskip
  174.   \leftskip=0pt \rightskip=0pt}
  175. \def\@changeBaselineskip{\baselineskip=\VDMbaselineskip
  176.   \lineskip=0pt \lineskiplimit=0pt
  177.   % need to alter the size of struts, too
  178.   \setbox\strutbox\hbox{\vrule height.7\baselineskip
  179.       depth.3\baselineskip width\z@}}
  180. % these are used in externals, records and cases
  181. \def\@changeLineSeparator{\let\\=\cr} % for usr within \halign
  182. \def\@restoreLineSeparator{\let\\=\newline}
  183. \def\@raggedRight{\rightskip=0pt plus 1fil
  184.   \hyphenpenalty=-100 \linepenalty=200
  185.   \binoppenalty=10000 \relpenalty=10000 \pretolerance=-1}
  186. %------------------------------------------------------------------------
  187. %    Font and Character Changes
  188. % make a-zA-Z use the \it family within math mode, and ~ mean \hook.
  189. % Digits 0-9 remain as normal.
  190. \newcount\@mathFamily  \@mathFamily=\itfam
  191. \everymath=\expandafter{\the\everymath\fam\@mathFamily
  192.     \@changeMathmodeCatcodes}
  193. \everydisplay=\expandafter{\the\everydisplay\fam\@mathFamily
  194.     \@changeMathmodeCatcodes}
  195. \mathcode`\0="0030
  196. \mathcode`\1="0031
  197. \mathcode`\2="0032
  198. \mathcode`\3="0033
  199. \mathcode`\4="0034
  200. \mathcode`\5="0035
  201. \mathcode`\6="0036
  202. \mathcode`\7="0037
  203. \mathcode`\8="0038
  204. \mathcode`\9="0039
  205. % If the user really wants the normal codes, she can call \defaultMathcodes
  206. \def\defaultMathcodes{\@mathFamily=-1}
  207. % make a : into punctuation, a - into a letter, and | mean \mid
  208. \ifps@
  209.  \def\@changeOtherMathcodes{\mathcode`\:="603A \mathcode`\-="002D
  210.   \mathcode`\|="327C \mathchardef\Or="32DA % this is a rel to get 5mu spacing
  211.   \mathcode`\f="0166} % normal letter spacing
  212. \else
  213.  \def\@changeOtherMathcodes{\mathcode`\:="603A \mathcode`\-="042D
  214.   \mathcode`\|="326A \mathchardef\Or="325F }% this is a rel to get 5mu spacing
  215. % alternative underscore
  216. \def\@VDMunderscore{\leavevmode
  217.   \kern.06em\vbox{\hrule\@height .2ex\@width .3em}\penalty\@postUnderPenalty
  218.   \hskip 0.1em}
  219. % Allow line breaks after an underscore, but not in vdm mode (see
  220. % \vdm).  This is so long identifiers can be broken when run
  221. % into paragraphs. 
  222. \newcount\@postUnderPenalty \@postUnderPenalty=200
  223. % now require some catcode trickery to enable us to change _ when we want to
  224. {\catcode`\_=\active \catcode`\"=\active
  225.  \gdef\@changeGlobalCatcodes{% make _ a normal char
  226.     \catcode`\_=\active \let_=\@VDMunderscore}
  227.  \gdef\@changeMathmodeCatcodes{%
  228.     % make ~ mean \hook, " do text, @ mean subscript
  229.     \let~=\hook
  230.     \catcode`\@=8
  231.     \catcode`\"=\active  \let"=\@mathText}
  232.  \gdef\underscoreoff{% make _ a normal char
  233.     \catcode`\_=\active \let_=\@VDMunderscore}
  234.  \gdef\underscoreon{% restore underscore to usual meaning
  235.     \catcode`\_=8}
  236.  \gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
  237. \def\mathTextFont{\rm}
  238. %----------------------------------------------------------------
  239. %    Keywords
  240. \ifx\fmtname\@fmtname
  241.     \def\keywordFontBeginSequence{\small\sf}%    user-definable
  242. \else\ifx\fmtname\@psfmtname
  243.     \def\keywordFontBeginSequence{\sf}%    user-definable
  244. \else
  245.     \def\keywordFontBeginSequence{\bf}%    good for SliTeX
  246. \fi\fi
  247. \def\kw#1{\hbox{\keywordFontBeginSequence #1\/}}
  248. \def\makeNewKeyword#1#2{% use \newcommand for extra checks
  249.     \newcommand{#1}{\hbox{\keywordFontBeginSequence #2\/}}}
  250. \makeNewKeyword{\nil}{nil}
  251. \makeNewKeyword{\True}{true}
  252. \makeNewKeyword{\true}{true}
  253. \makeNewKeyword{\False}{false}
  254. \makeNewKeyword{\false}{false}
  255. \def\where{\par\moveright\VDMindent\hbox{\keywordFontBeginSequence where\/}}
  256. %----------------------------------------------------------------
  257. %    monadic operator creation
  258. \def\newMonadicOperator#1#2{\newcommand{#1}{\kw{#2\kern.16667em}\nobreak}}
  259. %----------------------------------------------------------------
  260. %    primitive numeric types
  261. % use the AMS fonts for these if possible
  262. \ifams@
  263.   \mathchardef\Bool="0\msy@42    % Booleans
  264.   \mathchardef\Nat="0\msy@4E    % Natural numbers
  265.   \def\Nati{\Nat_1}        % Positive natural numbers
  266.   \mathchardef\Int="0\msy@5A    % Integers
  267.   \mathchardef\Real="0\msy@52    % Reals
  268.   \mathchardef\Rat="0\msy@51    % Rationals
  269. \else
  270.   \def\Bool{\hbox{\bf B\/}}
  271.   \def\Nat{\hbox{\bf N\/}}
  272.   \def\Nati{\hbox{$\hbox{\bf N}_1$}}
  273.   \def\Int{\hbox{\bf Z\/}}
  274.   \def\Real{\hbox{\bf R\/}}
  275.   \def\Rat{\hbox{\bf Q\/}}
  276. \let\Natone=\Nati % just for an alternative
  277. %----------------------------------------------------------------
  278. %    Operations
  279. % The op environment.  Within op you can specify args,
  280. % result, etc. which are gathered into registers, and output when the
  281. % op env. ends.
  282. % The optional argument is the operation name
  283. % shorthand for an operation on its own: the vdmop env.
  284. \def\vdmop{\vdm\op} \def\endvdmop{\endop\endvdm}
  285. % registers constructed within an op environment
  286. \newtoks\@operationName
  287. \newbox\@operationNameBox
  288. \newif\ifArgumentListEncountered@
  289. \newtoks\@argumentListTokens
  290. \newtoks\@resultNameAndTypeTokens
  291. \newbox\@externalsBox
  292. \newbox\@preConditionBox
  293. \newbox\@postConditionBox
  294. \def\op{% clear temporaries, deal with optional arg
  295.     \setbox\@operationNameBox=\hbox{}
  296.     \@argumentListTokens={} \ArgumentListEncountered@false
  297.     \@resultNameAndTypeTokens={}
  298.     \setbox\@externalsBox=\box\voidb@x
  299.     \setbox\@preConditionBox=\box\voidb@x
  300.     \setbox\@postConditionBox=\box\voidb@x
  301.     \par\preOperationHook
  302.     \vskip\preOperationSkip
  303.     \@beginVerticalVDM
  304.     \@ifnextchar [{\@opname}{}}
  305. % breaking parameters
  306. \newcount\preOperationPenalty \preOperationPenalty=0
  307. \newcount\preExternalPenalty \preExternalPenalty=2000
  308. \newcount\prePreConditionPenalty \prePreConditionPenalty=800
  309. \newcount\prePostConditionPenalty \prePostConditionPenalty=500
  310. \newcount\postOperationPenalty \postOperationPenalty=-500
  311. % gaps between bits of operations
  312. \newskip\preOperationSkip \preOperationSkip=2ex plus 0.5ex minus 0.2ex
  313. \newskip\postOperationSkip \postOperationSkip=2ex plus 0.5ex minus 0.2ex
  314. \newskip\postHeaderSkip \postHeaderSkip=.5ex plus .2ex minus .2ex
  315. \newskip\postExternalsSkip \postExternalsSkip=.5ex plus .2ex minus .2ex
  316. \newskip\postPreConditionSkip \postPreConditionSkip=.5ex plus .2ex minus .2ex
  317. \def\endop{% make up operation
  318.     % IMPORTANT---don't remove the vskips in this macro
  319.     % if you don't want one, set it to 0pt
  320.     \vskip 0pt
  321.     \@setOperationHeader
  322.     \betweenHeaderAndExternalsHook
  323.     \vskip\postHeaderSkip
  324.     \ifvoid\@externalsBox
  325.           \betweenExternalsAndPreConditionHook
  326.     \else \moveright\VDMindent\box\@externalsBox
  327.           \betweenExternalsAndPreConditionHook
  328.           \vskip\postExternalsSkip
  329.     \ifvoid\@preConditionBox
  330.           \betweenPreAndPostConditionHook
  331.     \else \moveright\VDMindent\box\@preConditionBox
  332.           \betweenPreAndPostConditionHook
  333.           \vskip\postPreConditionSkip
  334.     \ifvoid\@postConditionBox
  335.           \postOperationHook
  336.     \else \moveright\VDMindent\box\@postConditionBox
  337.           \postOperationHook
  338.           \vskip\postOperationSkip
  339.     \fi}
  340. % hooks for user-defined expansion
  341. % TeX is in outer vertical mode when these are called.
  342. % ALWAYS leave TeX in vertical mode after these macros have been called
  343. \def\preOperationHook{\penalty\preOperationPenalty }
  344. \def\betweenHeaderAndExternalsHook{\penalty\preExternalPenalty }
  345. \def\betweenExternalsAndPreConditionHook{\penalty\prePreConditionPenalty }
  346. \def\betweenPreAndPostConditionHook{\penalty\prePostConditionPenalty }
  347. \def\postOperationHook{\penalty\postOperationPenalty }
  348. % combine the operation name, argument list and result
  349. \def\@setOperationHeader{%
  350.     \moveright\VDMindent\vtop{%
  351.         \ifArgumentListEncountered@
  352.             \setbox\@operationNameBox=
  353.                 \hbox{\unhbox\@operationNameBox\ $($}\fi
  354.         \hangindent=\wd\@operationNameBox \hangafter=1
  355.         \noindent\kern-.05em\box\@operationNameBox
  356.         \@beginHorizontalVDM
  357.         \ifArgumentListEncountered@\the\@argumentListTokens)\fi
  358.         \ \the\@resultNameAndTypeTokens
  359.         \@endHorizontalVDM}}
  360. % set the operation name
  361. % \opname{name-of-operation}
  362. \def\opname#1{\@opname[#1]}
  363. \def\@opname[#1]{\@operationName={#1}%
  364.   \global\setbox\@operationNameBox=\hbox{$\relax#1$\ }}
  365. % set up the argument list
  366. % \args{ argument \\ argument \\ argument... } where \\ forces a line break
  367. % This is also used in the fn environment
  368. \def\args{\global\ArgumentListEncountered@true \global\@argumentListTokens=}
  369. % result name and type
  370. \def\res{\global\@resultNameAndTypeTokens=}
  371. % externals list
  372. % An external list could be either very long or very short, so we provide
  373. % two forms.  One is the short \ext{..} command, the other is the externals 
  374. % environment.
  375. % Externals are always separated by \\
  376. % we have to mess a little to get the catcode of : right
  377. \def\ext{\bgroup\@makeColonActive\@ext}
  378. \def\@ext#1{\externals#1\endexternals\egroup}
  379. \def\externals{\global\setbox\@externalsBox=%
  380.     \@beginIndentedPara{\hsize}{ext }{\@setUpExternals}}
  381. \def\endexternals{\@endIndentedPara{\@endAlignment}}
  382. \def\@setUpExternals{\@makeColonActive\@changeLineSeparator\@beginAlignment}
  383. % more catcode trickery for :
  384. {\catcode`\:=\active
  385.  \gdef\@makeColonActive{\catcode`\:=\active \let:=&}}
  386. % the \expandafters are necessary because TeX doesn't expand
  387. % \halign specs when scanning for # and &
  388. \def\@beginAlignment{\expandafter\halign\expandafter\bgroup
  389.     \the\@extAlign\strut\enspace&:\enspace$##$\hfil\cr}
  390. \def\@endAlignment{\crcr\egroup}
  391. % the user can decide on the exact alignment of the field names
  392. \newtoks\@extAlign
  393. \def\leftExternals{\@extAlign={$##$\hfil}}
  394. \def\rightExternals{\@extAlign={\hfil$##$}}
  395. \leftExternals
  396. \makeNewKeyword{\Rd}{rd } \makeNewKeyword{\Wr}{wr }
  397. % pre-condition and post-condition
  398. % once again we provide short forms \pre and \post, and environments
  399. % precond and postcond
  400. \def\pre#1{\precond#1\endprecond}
  401. \def\precond{\global\setbox\@preConditionBox=%
  402.     \@beginMathIndentedPara{\hsize}{pre }}
  403. \def\endprecond{\@endMathIndentedPara}
  404. \def\post#1{\postcond#1\endpostcond}
  405. \def\postcond{\global\setbox\@postConditionBox=%
  406.     \@beginMathIndentedPara{\hsize}{post }}
  407. \def\endpostcond{\@endMathIndentedPara}
  408. %----------------------------------------------------------------
  409. %    Box man\oe uvres
  410. % Here's where all the tricky box manipulation commands go
  411. % \@beginIndentedPara begins construction of a \hbox of width #1
  412. % which contains keyword #2 to the left of a para in a vtop.
  413. % #3 is evaluated within the inner vtop.
  414. % endIndentedPara closes the box off; its arg. is evaluated just
  415. % before closing the box.
  416. \def\@beginIndentedPara#1#2#3{\hbox to #1\bgroup \setbox0=\kw{#2}%
  417.     \copy0 \strut \vtop\bgroup \advance\hsize by -\wd0 #3}
  418. \def\@endIndentedPara#1{\strut#1\egroup\hss\egroup}
  419. % \@beginMathIndentedPara places the para in vdm mode
  420. \def\@beginMathIndentedPara#1#2{\@beginIndentedPara{#1}{#2}%
  421.     {\@beginHorizontalVDM}}
  422. \def\@endMathIndentedPara{\@endIndentedPara{\@endHorizontalVDM}}
  423. % \@belowAndIndent#1#2 places #2 in a vbox below and to the right of #1
  424. \def\@belowAndIndent#1#2{#1\hfil\break
  425.     \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
  426. %----------------------------------------------------------------
  427. %    Constructions
  428. % Here are all the standard constructions.
  429. % The only tricky one is \cases.
  430. % Those that construct a box must be made to make that box of 0 width,
  431. % and force a line break immediately afterwards.
  432. % \If mm-exp \Then mm-exp \Else mm-exp \Fi
  433. % multi-line indented if-then-else
  434. \def\If#1\Then#2\Else#3\Fi{\vtop{%
  435.     \@beginMathIndentedPara{0pt}{if }#1\@endMathIndentedPara
  436.     \@beginMathIndentedPara{0pt}{then }#2\@endMathIndentedPara
  437.     \@beginMathIndentedPara{0pt}{else }#3\@endMathIndentedPara}}
  438. % \SIf mm-exp \Then mm-exp \Else mm-exp \Fi
  439. % single line if-then-else
  440. \def\SIf#1\Then#2\Else#3\Fi{\hbox to 0pt{\vtop{\@beginHorizontalVDM
  441.     \kw{if }\nobreak#1\penalty0\hskip 0.5em
  442.     \kw{then }\nobreak#2\penalty-100\hskip 0.5em % break here OK
  443.     \kw{else }\nobreak#3\@endHorizontalVDM}\hss}\hfil\break}
  444. % \Let mm-exp \In mm-exp2
  445. % multi-line let..in ; mm-exp2 is `curried'
  446. \def\Let#1\In{\vtop{%
  447.     \@beginMathIndentedPara{0pt}{let }#1\hskip 0.5em
  448.     \kw{in}\@endMathIndentedPara}\hfil\break}
  449. % \SLet mm-exp \In mm-exp
  450. % single-line let..in
  451. \def\SLet#1\In#2{\hbox to 0pt{\vtop{\@beginHorizontalVDM
  452.     \kw{let }\nobreak#1\hskip 0.5em
  453.     \kw{in }\penalty-200 #2\@endHorizontalVDM}\hss}\hfil\break}
  454. % multi-line cases
  455. % \Cases{ selecting-mm-exp }
  456. % from-case1 & to-case1 \\
  457. % from-case2 & to-case2 \\
  458. %        ...
  459. % from-casen & to-casen
  460. % \Otherwise{ mm-exp }
  461. % \Endcases[optional text for the rest of the line]
  462. \newif\ifOtherwiseEncountered@
  463. \newtoks\@OtherwiseTokens
  464. \def\Cases#1{\hbox to 0pt\bgroup \vtop\bgroup
  465.         \@beginMathIndentedPara{\hsize}{cases }\strut
  466.             #1\hskip 0.5em\strut\kw{of}%
  467.         \@endMathIndentedPara
  468.         \bgroup % we might be in a nested case, so we have to
  469.             % save the \Otherwise bits we might lose
  470.         \OtherwiseEncountered@false \@changeLineSeparator 
  471.         \@beginCasesAlignment}
  472. % the user can decide on the exact alignment
  473. \newtoks\@casesDef
  474. \def\leftCases{\@casesDef={$##$\hfil}}
  475. \def\rightCases{\@casesDef={\hfil$##$}}
  476. \rightCases
  477. % the \expandafters are necessary because TeX doesn't expand
  478. % \halign specs when scanning for # and &
  479. \def\@beginCasesAlignment{\expandafter\halign\expandafter\bgroup
  480.     \the\@casesDef&$\,\rightarrow##$\hfil\cr}
  481. \def\Otherwise{\global\OtherwiseEncountered@true \global\@OtherwiseTokens=}
  482. \def\Endcases{\@endCasesAlignment \@setOtherwise \egroup \@setEndcases}
  483. \def\@endCasesAlignment{\crcr\egroup}
  484. \def\@setOtherwise{\ifOtherwiseEncountered@ % have an otherwise clause
  485.     \@beginMathIndentedPara{\hsize}{otherwise }%
  486.     \strut\the\@OtherwiseTokens\strut
  487.     \@endMathIndentedPara
  488.     \fi}
  489. % must test for the optional arg to follow the end
  490. \def\@setEndcases{\noindent
  491.     \strut\kw{end}\@ifnextchar [{\@unbracket}{\@finalCaseEnd}}
  492. \def\@unbracket[#1]{$#1$\@finalCaseEnd}
  493. \def\@finalCaseEnd{\egroup\hss\egroup\hfil\break}
  494. %----------------------------------------------------------------
  495. %    special symbols
  496. % defined as
  497. \ifps@
  498.  \def\DEF{\raise.5ex
  499.     \hbox{\footnotesize\underline{$\mathchar"3\cmsy@34$}}}% a \triangle
  500. \else
  501.  \def\DEF{\raise.5ex
  502.     \hbox{\footnotesize\underline{$\mathchar"3234$}}}% a \triangle
  503. % cross product
  504. \let\x=\times
  505. %    logical connectives
  506. \def\Iff{\penalty-50\mskip 7mu plus 2mu minus 2mu
  507.     \Leftrightarrow\mskip 7mu plus 2mu minus 2mu}
  508. \let\iff=\Iff
  509. \def\Implies{\penalty-35\mskip 6mu plus 2mu minus 1mu \Rightarrow
  510.     \mskip 6mu plus 2mu minus 1mu}
  511. \let\implies=\Implies
  512. % see changeOtherMathcodes for \Or
  513. \let\And=\land
  514. \let\and=\And
  515. %  use \neg for logical not, or
  516. \let\Not=\neg
  517. %    quantification
  518. \ifps@
  519.  \mathchardef\Exists="0224
  520.  \mathchardef\Forall="0222
  521.  \mathchardef\suchthat="22D7
  522. \else
  523.  \mathchardef\Exists="0239
  524.  \mathchardef\Forall="0238
  525.  \mathchardef\suchthat="2201
  526. \def\exists{\@ifstar{\@splitExists}{\@normalExists}}
  527. \ifams@
  528.   \mathchardef\@nexists="0\msy@40 % crossed out existential quantifier
  529. \else
  530.   \def\@nexists{\hbox to 0pt{\raise0.15ex\hbox{/}\hss}\Exists}
  531. \def\nexists{\@ifstar{\@splitNExists}{\@normalNExists}}
  532. \def\forall{\@ifstar{\@splitForall}{\@normalForall}}
  533. \def\unique{\@ifstar{\@splitUnique}{\@normalUnique}}
  534. \def\uniqueval{\@ifstar{\@splitUniqueval}{\@normalUniqueval}}
  535. \def\@normalExists#1#2{{\Exists#1}\suchthat #2}
  536. \def\@normalNExists#1#2{{\@nexists#1}\suchthat #2}
  537. \def\@normalForall#1#2{{\Forall#1}\suchthat #2}
  538. \def\@normalUnique#1#2{{\Exists!\,#1}\suchthat #2}
  539. \def\@normalUniqueval#1#2{{\iota\,#1}\suchthat #2}
  540. \def\@splitExists#1{\@belowAndIndent{\Exists#1\suchthat}}
  541. \def\@splitNExists#1{\@belowAndIndent{\@nexists#1\suchthat}}
  542. \def\@splitForall#1{\@belowAndIndent{\Forall#1\suchthat}}
  543. \def\@splitUnique#1{\@belowAndIndent{\Exists!\,#1\suchthat}}
  544. \def\@splitUniqueval#1{\@belowAndIndent{\iota\,#1\suchthat}}
  545. %    strachey brackets
  546. % (see TeXbook, p.437)
  547. \def\term#1{[\mkern-\thinmuskip[#1\relax]\mkern-\thinmuskip]}
  548. %    function composition
  549. \let\compf=\circ
  550. %----------------------------------------------------------------
  551. %    function environment
  552. % This environment is similar to the op environment, but is used for
  553. % function definition.  
  554. % The mandatory first parameter is the name of the function, the
  555. % second is the argument list.
  556. % The *-form simply doesn't force the parentheses round the argument list
  557. \def\fn{\parens@true\@beginVDMfunction}
  558. \@namedef{fn*}{\parens@false\@beginVDMfunction}
  559. \@namedef{endfn*}{\endfn}
  560. % short form
  561. \def\vdmfn{\vdm\parens@true \@beginVDMfunction}
  562. \def\endvdmfn{\endfn\endvdm}
  563. \@namedef{vdmfn*}{\vdm\parens@false \@beginVDMfunction}
  564. \@namedef{endvdmfn*}{\endfn\endvdm}
  565. % registers used within the fn environment
  566. \newtoks\@fnName
  567. \newbox\@fnNameBox
  568. \newif\ifsignatureEncountered@
  569. \newtoks\@signatureTokens
  570. \newbox\@fnDefnBox
  571. \newif\ifparens@
  572. \def\@beginVDMfunction#1#2{%
  573.     \@fnName={#1}
  574.     \setbox\@fnNameBox=\hbox{$#1$}%
  575.     \setbox\@preConditionBox=\box\voidb@x % for people who want to do
  576.     \setbox\@postConditionBox=\box\voidb@x% implicit defns
  577.     \@signatureTokens={}\signatureEncountered@false
  578.     \ifparens@
  579.         \@argumentListTokens={(#2)}%
  580.     \else
  581.         \@argumentListTokens={#2}%
  582.     \par\preFunctionHook
  583.     \vskip\preFunctionSkip
  584.     \@beginVerticalVDM 
  585.     \@beginFnDefn}
  586. % read in a signature
  587. \def\signature{\global\signatureEncountered@true \global\@signatureTokens=}
  588. \def\@beginFnDefn{\global\setbox\@fnDefnBox=\vtop\bgroup
  589.     \hangindent=2em \hangafter=1 \@beginHorizontalVDM
  590.     \advance\hsize by-2em % this fools vboxes within the
  591.     % function body about the hanging indent...yuk.
  592.     % If you change the size of the indent, change the
  593.     % corresponding line in \endfn.
  594.     \copy\@fnNameBox \the\@argumentListTokens 
  595.     \quad\DEF\penalty-100\quad }
  596. \newskip\preFunctionSkip \preFunctionSkip=2ex plus .5ex minus .2ex
  597. \newskip\postFunctionSkip \postFunctionSkip=2ex plus .5ex minus .2ex
  598. \newskip\betweenSignatureAndBodySkip
  599. \betweenSignatureAndBodySkip=1.2ex plus .3ex minus .2ex
  600. \newskip\betweenFunctionAndPreSkip
  601. \betweenFunctionAndPreSkip=1.2ex plus .3ex minus .2ex
  602. \def\endfn{%
  603.     \advance\hsize by 2em% matches the dirty \advance in \@beginFnDefn
  604.     \@endHorizontalVDM
  605.     \egroup  % this ends the vtop we started in \@beginFnDefn
  606.     \ifsignatureEncountered@
  607.         \setbox0=\hbox{\unhbox\@fnNameBox$\;\mathpunct:\,$}%
  608.         \dimen255=\wd0 \noindent \box0
  609.         \vtop{\advance\hsize by-\dimen255 \@beginHorizontalVDM
  610.             \the\@signatureTokens \@endHorizontalVDM}\par
  611.         \betweenSignatureAndBodyHook
  612.         \vskip\betweenSignatureAndBodySkip
  613.     \moveright\VDMindent\box\@fnDefnBox
  614.     \ifvoid\@preConditionBox
  615.           \betweenPreAndPostConditionHook
  616.           \vskip\postFunctionSkip
  617.     \else \betweenFunctionAndPreHook
  618.           \vskip\betweenFunctionAndPreSkip
  619.           \moveright\VDMindent\box\@preConditionBox
  620.           \betweenPreAndPostConditionHook
  621.           \vskip\postPreConditionSkip
  622.     \ifvoid\@postConditionBox
  623.           \postFunctionHook
  624.     \else \moveright\VDMindent\box\@postConditionBox
  625.           \postFunctionHook
  626.           \vskip\postOperationSkip
  627.     \fi}
  628. \newcount\preFunctionPenalty \preFunctionPenalty=0
  629. \newcount\betweenSignatureAndBodyPenalty \betweenSignatureAndBodyPenalty=500
  630. \newcount\betweenFunctionAndPrePenalty \betweenFunctionAndPrePenalty=1000
  631. \newcount\postFunctionPenalty \postFunctionPenalty=-500
  632. % These are called in outer vertical mode---they must also exit in this mode
  633. \def\preFunctionHook{\penalty\preFunctionPenalty }
  634. \def\betweenSignatureAndBodyHook{\penalty\betweenSignatureAndBodyPenalty }
  635. \def\betweenFunctionAndPreHook{\penalty\betweenFunctionAndPrePenalty }
  636. \def\postFunctionHook{\penalty\postFunctionPenalty }
  637. %    other function-related things
  638. % function arrow
  639. \def\to{\penalty-100\rightarrow}
  640. % explicit lamdba function
  641. \def\LambdaFn{\@ifstar{\@splitLambdaFn}{\@normalLambdaFn}}
  642. \def\@normalLambdaFn#1#2{{\lambda#1}\suchthat#2}
  643. \def\@splitLambdaFn#1#2{% place body in a separate box below and to the right
  644.     {\lambda#1}\suchthat\hfil\break
  645.     \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
  646. %----------------------------------------------------------------
  647. %    Sets
  648. % new set type
  649. \def\setof#1{\kw{set of }#1}
  650. % set enumeration
  651. \def\set#1{\{#1\}}
  652. % empty set
  653. \def\emptyset{\{\,\}}
  654. % usual LaTeX operators apply: \in \notin \subset \subseteq
  655. \let\inter=\cap \let\intersection=\inter
  656. \let\Inter=\bigcap \let\Intersection=\Inter
  657. \let\union=\cup
  658. \let\Union=\bigcup
  659. \ifps@
  660.  \mathchardef\minus="222D
  661. \else
  662.  \mathchardef\minus="2200
  663. \def\diff{\minus} \let\difference=\diff
  664. \newMonadicOperator{\card}{card}
  665. \newMonadicOperator{\Min}{min}
  666. \newMonadicOperator{\Max}{max}
  667. %----------------------------------------------------------------
  668. %     Map type
  669. % new map type
  670. \def\mapof#1#2{\kw{map }\nobreak#1\penalty-50\hskip .3em \kw{to }\nobreak#2}
  671. % one-one map
  672. \def\mapinto#1#2{\kw{map }\nobreak#1\penalty-50
  673.     \hskip .3em \kw{into }\nobreak#2}
  674. % map enumeration
  675. \def\map#1{\{#1\}}
  676. % empty map
  677. \def\emptymap{\{\,\}}
  678. %    map operators
  679. % use \mapsto for |->
  680. % overwrite
  681. \def\owr{\dagger}
  682. \ifams@
  683.   % domain restriction
  684.   \mathchardef\dres="2\msx@43
  685.   % range restriction
  686.   \mathchardef\rres="2\msx@42 % the right hand version
  687. \else % for those without AMS fonts
  688.   \let\dres=\lhd
  689.   \let\rres=\rhd
  690. % domain subtraction
  691. \ifps@
  692.  \def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu\dres$}}}
  693. \else
  694.  \def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
  695.     \lower.1ex\hbox{$\dres$}$}}}
  696. % range subtraction
  697. \ifps@
  698.  \def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu\rres$}}}
  699. \else
  700.  \def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
  701.     \lower.1ex\hbox{$\rres$}$}}}
  702. \newMonadicOperator{\dom}{dom}
  703. \newMonadicOperator{\rng}{rng}
  704. %----------------------------------------------------------------
  705. %    Sequences
  706. % new type
  707. \def\seqof#1{\kw{seq of }#1}
  708. % enumeration
  709. \def\seq#1{[#1]}
  710. % empty sequence
  711. \def\emptyseq{[\,]}
  712. \newMonadicOperator{\len}{len}
  713. \newMonadicOperator{\hd}{hd}
  714. \newMonadicOperator{\tl}{tl}
  715. \newMonadicOperator{\elems}{elems}
  716. \newMonadicOperator{\inds}{inds}
  717. \def\cons#1{\kw{cons}\nobreak(#1)}
  718. % sequence concatenation
  719. \ifams@
  720.   \mathchardef\sconc="2\msy@79
  721. \else
  722.   % this is truly yukky
  723.   \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\frown$}\kern-0.47em
  724.     \raise0.2ex\hbox{\it\char"12}}}}
  725. % distributed concatenation
  726. \newMonadicOperator{\Conc}{conc}
  727. %----------------------------------------------------------------
  728. %    type equation
  729. \newtoks\@typeName
  730. \def\type#1#2{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
  731.     \@beginVerticalVDM
  732.     \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2
  733.         \@endHorizontalVDM}
  734.     \postTypeHook \vskip\postTypeSkip}}
  735. \def\preTypeHook{} \def\postTypeHook{}
  736. \newskip\preTypeSkip \preTypeSkip=1.2ex plus .5ex minus .3ex
  737. \newskip\postTypeSkip \postTypeSkip=1.2ex plus .5ex minus .3ex
  738. %----------------------------------------------------------------
  739. %    Composite Objects
  740. % literal composition; we have a compose and a composite env.
  741. % single line compose
  742. \@namedef{composite*}#1{\kw{compose }$\relax#1\relax$\kw{ of }$\relax}
  743. \@namedef{endcomposite*}{\relax$\kw{ end}}
  744. % multiple line version
  745. \def\composite#1{\bgroup\vskip\preCompositeSkip
  746.     \@beginVerticalVDM
  747.     \moveright\VDMindent\vtop\bgroup
  748.     \@beginHorizontalVDM
  749.     \kw{compose }#1\kw{ of}%\hfil\break
  750.     \@endHorizontalVDM
  751.     \@makeColonActive\@changeLineSeparator
  752.     \expandafter\halign\expandafter\bgroup\expandafter\qquad
  753.         \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
  754. \def\endcomposite{\crcr\egroup % closes \halign
  755.     \kw{end}\egroup % ends the \vtop
  756.     \vskip\postCompositeSkip\egroup}
  757. \def\scompose#1#2{\@nameuse{composite*}{#1}{#2}\@nameuse{endcomposite*}}
  758. \newskip\preCompositeSkip \preCompositeSkip=1.2ex plus .5ex minus .3ex
  759. \newskip\postCompositeSkip \postCompositeSkip=1.2ex plus .5ex minus .3ex
  760. % record composites; likewise we have a short and a long form
  761. \newtoks\@recordName
  762. \def\record#1{\@recordName{#1}
  763.   \par\preRecordHook
  764.   \vskip\preRecordSkip
  765.   \@beginVerticalVDM
  766.   \moveright\VDMindent\hbox\bgroup
  767.       \setbox0=\hbox{$#1$\enspace::\enspace}%
  768.       \@makeColonActive\@changeLineSeparator
  769.       \advance\hsize by-\wd0 \box0
  770.       \@restoreMargins
  771.       % the \expandafters are necessary because TeX doesn't expand
  772.       % \halign specs when scanning for # and &
  773.       \vtop\bgroup\expandafter\halign\expandafter\bgroup
  774.           \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
  775. \def\endrecord{\crcr\egroup% closes halign
  776.     \egroup% closes vtop
  777.     \egroup% closes hbox
  778.     \par\postRecordHook
  779.     \vskip\postRecordSkip}
  780. % the user can decide on the exact alignment of the field names
  781. \newtoks\@recordAlign
  782. \def\leftRecord{\@recordAlign={$##$\hfil}}
  783. \def\rightRecord{\@recordAlign={\hfil$##$}}
  784. \rightRecord
  785. % more catcode trickery
  786. \def\defrecord{\bgroup\@makeColonActive\@defrecord}
  787. \def\@defrecord#1#2{\record{#1}#2\endrecord\egroup}
  788. \newskip\preRecordSkip \preRecordSkip=.75ex plus .3ex minus .2ex
  789. \newskip\postRecordSkip \postRecordSkip=.75ex plus .3ex minus .2ex
  790. \newcount\preRecordPenalty \preRecordPenalty=0
  791. \newcount\postRecordPenalty \postRecordPenalty=-100
  792. \def\preRecordHook{\penalty\preRecordPenalty }
  793. \def\postRecordHook{\penalty\postRecordPenalty }
  794. % \chg: mu function on composites
  795. \def\chg#1#2#3{\mu(#1,#2\mapsto#3)}
  796. %----------------------------------------------------------------
  797. %    Hooks
  798. % hooked identifiers --- these are taken from the TeXbook, p.357, 359
  799. \ifps@
  800.  \def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
  801.   \cleaders\hbox{$\mkern-2mu \mathchar"0\cmsy@00 \mkern-2mu$}\hfill
  802.   \mkern-6mu \mathchar"0\cmsy@00$}  % p.357, \leftarrowfill
  803. \else
  804.  \def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
  805.   \cleaders\hbox{$\mkern-2mu \mathord\minus \mkern-2mu$}\hfill
  806.   \mkern-6mu \mathord\minus$}  % p.357, \leftarrowfill
  807. \def\overleftharpoonup#1{{%
  808.   \boxmaxdepth=\maxdimen % this fixes Lamport's figures, but isn't necessary
  809.                % for versions after 15 Dec 87
  810.   \vbox{\ialign{##\crcr % p.359, \overleftarrow
  811.     \leftharpoonupfill\crcr\noalign{\kern-\p@\nointerlineskip}
  812.     $\hfil\displaystyle{#1}\hfil$\crcr}}}}
  813. \let\hook=\overleftharpoonup  % c'est simple comme bonjour
  814. %-----------------------------------------------------------------
  815. %     General formula environment, a bit like \[ \] but is
  816. %    indented to \VDMindent and will take \\
  817. \def\form#1{\formula #1\endformula}
  818. \def\formula{\par\preFormulaHook
  819.     \vskip\preFormulaSkip
  820.     \@beginVerticalVDM
  821.     \bgroup
  822.     \moveright\VDMindent\vtop\bgroup\@beginHorizontalVDM}
  823. \def\endformula{\@endHorizontalVDM\egroup % ends the vtop
  824.     \egroup % ends the overall group
  825.     \par\postFormulaHook
  826.     \vskip\postFormulaSkip}
  827. \newskip\preFormulaSkip \preFormulaSkip=1.2ex plus .5ex minus .3ex
  828. \newskip\postFormulaSkip \postFormulaSkip=1.2ex plus .5ex minus .3ex
  829. \newcount\preFormulaPenalty \preFormulaPenalty=0
  830. \newcount\postFormulaPenalty \postFormulaPenalty=-100
  831. \def\preFormulaHook{\penalty\preFormulaPenalty }
  832. \def\postFormulaHook{\penalty\postFormulaPenalty }
  833. %----------------------------------------------------------------
  834. %    Formula within a box, when width is unknown
  835. %    equivalent to \parbox[t]{\hsize}{\@beginHorizontalVDM
  836. %        ...\@endHorizontalVDM}
  837. \def\formbox{\vtop\bgroup\@beginHorizontalVDM}
  838. \def\endformbox{\strut\@endHorizontalVDM\egroup}
  839. %----------------------------------------------------------------
  840. %    special font for constants
  841. \def\constantFont{\sc}
  842. \def\const#1{\hbox{\constantFont #1\/}}
  843. %----------------------------------------------------------------
  844. %    line break and indent
  845. \def\T#1{\\\hbox to #1em{}}
  846. %----------------------------------------------------------------
  847. %    line break and push line after to RHS
  848. \def\R{\\\hspace*{\fill}}
  849. %----------------------------------------------------------------
  850. %    Proofs
  851. % a proof environment for typesetting proofs in the "natural
  852. % deduction" style.
  853. \newdimen\ProofIndent \ProofIndent=\VDMindent
  854. \newdimen\ProofNumberWidth \ProofNumberWidth=\parindent
  855. \def\proof{\par\preProofHook
  856.     \vskip\preProofSkip
  857.     \let\&=\@proofLine
  858.     \moveright\ProofIndent\vtop\bgroup
  859.         \@indentLevel=1
  860.         \advance\linewidth by-\ProofIndent
  861.         \begin{tabbing}%
  862.         \hbox to\ProofNumberWidth{}\=\kill}    % template line
  863. \def\endproof{\end{tabbing}\advance\linewidth by\ProofIndent
  864.     \egroup % ends the \vtop
  865.     \par\postProofHook
  866.     \vskip\postProofSkip}
  867. \newskip\preProofSkip \preProofSkip=1.2ex plus .5ex minus .3ex
  868. \newskip\postProofSkip \postProofSkip=1.2ex plus .5ex minus .3ex
  869. \newcount\preProofPenalty \preProofPenalty=-100
  870. \newcount\postProofPenalty \postProofPenalty=0
  871. \def\preProofHook{\penalty\preProofPenalty }
  872. \def\postProofHook{\penalty\postProofPenalty }
  873. \def\From{\@indentProof\kw{from }\=%
  874.     \global\advance\@indentLevel by 1
  875.     \@enterMathMode}
  876. \def\Infer{\global\advance\@indentLevel by-1
  877.     \@indentProof\kw{infer }\@enterMathMode}
  878. \def\@proofLine{\@indentProof\@enterMathMode}
  879. \def\by{\`}
  880. \newcount\@indentLevel
  881. \newcount\@indentCount
  882. \def\@indentProof{% do \>, \@indentLevel times
  883.     \global\@indentCount=\@indentLevel
  884.     \@gloop \>\global\advance\@indentCount by-1
  885.     \ifnum\@indentCount>0
  886.     \repeat}
  887. % need special loop macros that works in across boxes
  888. \def\@gloop#1\repeat{\gdef\@body{#1}\@giterate}
  889. \def\@giterate{\@body \global\let\@gloopNext=\@giterate
  890.     \else \global\let\@gloopNext=\relax \fi \@gloopNext}
  891. % this enters math mode and sets the LaTeX macros \@stopfield up
  892. % to exit math mode
  893. \def\@enterMathMode{\def\@stopfield{$\egroup}$}
  894. %----------------------------------------------------------------
  895. \def\VDMauthor{M.Wolczko,
  896. CS Dept.,
  897. Univ. of Manchester, UK. 
  898. mario@uk.ac.man.cs.ux
  899. mcvax!man.cs.r5!mario}
  900. \def\VDMversion{2.5}
  901. \typeout{vdm style option <25 Mar 88>}
  902. %----------------------------------------------------------------
  903. %    Global changes
  904. % All things that have to be invoked before the user's stuff appears
  905. % should go here.
  906. % by default the math spacing and changes to @ and _ apply everywhere
  907. \@changeOtherMathcodes \@changeGlobalCatcodes
  908. %-------------------the end--------------------------------------
  909. \endinput
  910. %    Summary of penalties
  911. %    Penalties in vertical mode
  912. % \preOperationPenalty        before an op begins
  913. % \preExternalPenalty        between the header and externals of an op
  914. % \prePreConditionPenalty    before the precondition
  915. % \prePostConditionPenalty    before the postcondition
  916. % \postOperationPenalty        at the end of an op
  917. % \preFunctionPenalty        before a fn begins
  918. % \betweenSignatureAndBodyPenalty 
  919. % \postFunctionPenalty        after a fn ends
  920. % \preRecordPenalty        before a record
  921. % \postRecordPenalty        after a record
  922. %    etc for formula, proof
  923. %    Penalties in horizontal mode in boxes
  924. % \linepenalty            101        \@raggedRight
  925. % `if mm-exp ^ then..'        0        \SIf
  926. % `if ... then mm-exp ^ else'    -100        \SIf
  927. % `let mm-exp in ^ ...'        -200        \SLet
  928. % `map mm-exp ^ to ...'        -50        \map
  929. % ^\iff                -50        \iff
  930. % ^\implies            -35        \implies
  931. % func(args) \DEF^        -100        \begin{fn}
  932. % \binoppenalty            10000
  933. % \relpenalty            10000
  934. % \hyphenpenalty        -100        \suchthat
  935. % ^\to                -100        \to
  936. % _^                100        \@VDMunderscore
  937.